Java Modeling Language
part 3/4 · 12.1 KB total
──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
//@ assignable balance;
//@ ensures balance == 0;
public BankingExample()
{
this.balance = 0;
}
//@ requires 0 < amount && amount + balance < MAX_BALANCE;
//@ assignable balance;
//@ ensures balance == \old(balance) + amount;
public void credit(final int amount)
{
this.balance += amount;
}
//@ requires 0 < amount && amount <= balance;
//@ assignable balance;
//@ ensures balance == \old(balance) - amount;
public void debit(final int amount)
{
this.balance -= amount;
}
//@ ensures isLocked == true;
public void lockAccount()
{
this.isLocked = true;
}
//@ requires !isLocked;
//@ ensures \result == balance;
//@ also
//@ requires isLocked;
//@ signals_only BankingException;
public /*@ pure @*/ int getBalance() throws BankingException
{
if (!this.isLocked)
{
return this.balance;
}
else
{
throw new BankingException();
}
}
}
Full documentation of JML syntax is available in the JML Reference Manual.
Tool support
A variety of tools provide functionality based on JML annotations. The Iowa State JML tools provide an assertion checking compiler jmlc which converts JML annotations into runtime assertions, a documentation generator jmldoc which produces Javadoc documentation augmented with extra information from JML annotations, and a unit test generator jmlunit which generates JUnit test code from JML annotations.
Independent groups are working on tools that make use of JML annotations. These include:
• ESC/Java2 [1], an extended static checker which uses JML annotations to perform more rigorous static checking than is otherwise possible.
• OpenJML declares itself the successor of ESC/Java2.
• Daikon, a dynamic invariant generator.
• KeY, which provides an open source theorem prover with a JML front-end and an Eclipse plug-in (JML Editing) with support for syntax highlighting of JML.
• Krakatoa, a static verification tool based on the Why verification platform and using the Coq proof assistant.
• JMLEclipse, a plugin for the Eclipse integrated development environment with support for JML syntax and interfaces to various tools that make use of JML annotations.
• Sireum/Kiasan, a symbolic execution based static analyzer which supports JML as a contract language.
• JMLUnit, a tool to generate files for running JUnit tests on JML annotated Java files.
──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────